i, x:Id, a, b, c:Knd, T:Type.
@i: only members of [a; b; c] affect x :T  Dsys
& (D:Dsys.
& (@i: only members of [a; b; c] affect x :T  D
& ( D 
& ( realizes es.
& ( vartype(i;x)  T
& ( & e@i.
& ( & ((x after e) = (x when e)  T  kind(e) = a  Knd  kind(e) = b  Knd  kind(e) = c  Knd)
& ( & & (kind(e) = a
& ( & & ( kind(e) = b  Knd
& ( & & ( kind(e) = c  Knd
& ( & & ( (x after e) = (x when e)  T)) 

latex

Definitions	x:A. B(x), A & B, t  T, P  Q, D realizes es. P(es), e@i. P(e), P & Q, A, P  Q, P  Q, Prop, P  Q, {T}, @i only events in L change   x : T, False, Dec(P)
Lemmas	s-frame-rule, es-vartype wf, implies functionality wrt iff, not wf, l member wf, es-kind wf, es-after wf, es-when wf, not functionality wrt iff, cons member, or functionality wrt iff, false wf, nil member, decidable or, decidable equal Kind, Knd wf, w-es wf, es-E wf, fair-fifo wf, world wf, es-loc wf, possible-world wf, d-sub wf, dsys wf, Id wf